This paper studies motion planning of a mobile robot under uncertainty. Thecontrol objective is to synthesize a {finite-memory} control policy, such thata high-level task specified as a Linear Temporal Logic (LTL) formula issatisfied with a desired high probability. Uncertainty is considered in theworkspace properties, robot actions, and task outcomes, giving rise to a MarkovDecision Process (MDP) that models the proposed system. Different from mostexisting methods, we consider cost optimization both in the prefix and suffixof the system trajectory. We also analyze the potential trade-off betweenreducing the mean total cost and maximizing the probability that the task issatisfied. The proposed solution is based on formulating two coupled LinearPrograms, for the prefix and suffix, respectively, and combining them into amulti-objective optimization problem, which provides provable guarantees on theprobabilistic satisfiability and the total cost optimality. We show that ourmethod outperforms relevant approaches that employ Round-Robin policies in thetrajectory suffix. Furthermore, we propose a new control synthesis algorithm tominimize the frequency of reaching a bad state when the probability ofsatisfying the tasks is zero, in which case most existing methods return nosolution. We validate the above schemes via both numerical simulations andexperimental studies.
展开▼
